Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data.

Stochastic population models are widely used to model phenomena in different areas such as cyber-physical systems, chemical kinetics, collective animal behaviour, and beyond. Quantitative analysis of stochastic population models easily becomes challenging due to the combinatorial number of possible states of the population. Moreover, while the modeller easily hypothesises the mechanistic aspects of the model, the quantitative parameters associated to these mechanistic transitions are difficult or impossible to measure directly. In this paper, we investigate how formal verification methods can aid parameter inference for population discrete-time Markov chains in a scenario where only a limited sample of population-level data measurements-sample distributions among terminal states-are available. We first discuss the parameter identifiability and uncertainty quantification in this setup, as well as how the existing techniques of formal parameter synthesis and Bayesian inference apply. Then, we propose and implement four different methods, three of which incorporate formal parameter synthesis as a pre-computation step. We empirically evaluate the performance of the proposed methods over four representative case studies. We find that our proposed methods incorporating formal parameter synthesis as a pre-computation step allow us to significantly enhance the accuracy, precision, and scalability of inference. Specifically, in the case of unidentifiable parameters, we accurately capture the subspace of parameters which is data-compliant at a desired confidence level.

Extracting individual characteristics from population data reveals a negative social effect during honeybee defence.

Honeybees protect their colony against vertebrates by mass stinging and they coordinate their actions during this crucial event thanks to an alarm pheromone carried directly on the stinger, which is therefore released upon stinging. The pheromone then recruits nearby bees so that more and more bees participate in the defence. However, a quantitative understanding of how an individual bee adapts its stinging response during the course of an attack is still a challenge: Typically, only the group behaviour is effectively measurable in experiment; Further, linking the observed group behaviour with individual responses requires a probabilistic model enumerating a combinatorial number of possible group contexts during the defence; Finally, extracting the individual characteristics from group observations requires novel methods for parameter inference. We first experimentally observed the behaviour of groups of bees confronted with a fake predator inside an arena and quantified their defensive reaction by counting the number of stingers embedded in the dummy at the end of a trial. We propose a biologically plausible model of this phenomenon, which transparently links the choice of each individual bee to sting or not, to its group context at the time of the decision. Then, we propose an efficient method for inferring the parameters of the model from the experimental data. Finally, we use this methodology to investigate the effect of group size on stinging initiation and alarm pheromone recruitment. Our findings shed light on how the social context influences stinging behaviour, by quantifying how the alarm pheromone concentration level affects the decision of each bee to sting or not in a given group size. We show that recruitment is curbed as group size grows, thus suggesting that the presence of nestmates is integrated as a negative cue by individual bees. Moreover, the unique integration of exact and statistical methods provides a quantitative characterisation of uncertainty associated to each of the inferred parameters.